($b$?$x$) $\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$if $b$$\rightarrow$ inl($x$) else inr($\cdot$) fi